Nuprl Lemma : assert-w-isrcvl 11,40
the_w:World, l:IdLnk, i:Id, a:Action(i).
(isrcv(l;a))  {((isnull(a))) & (isrcv(kind(a))) & lnk(kind(a)) = l} 
latex

Definitionsx:A. B(x), P  Q, b, isrcv(l;a), {T}, P & Q, A, p  q, b, t  T, tt, if b then t else f fi , ff, True, , , Unit, P  Q, False,
Lemmasw-isnull wf, bool wf, eqtt to assert, false wf, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, isrcv wf, w-kind wf, assert-eq-lnk, lnk wf, w-isrcvl wf, w-action wf, Id wf, IdLnk wf, world wf

origin